package preuve;

import base.Formule;

public class Preuve {
	
	/*
	 * Attributs
	 */
	
	private Formule premisses;
	private Formule conclusion;
	
	/*
	 * Constructeur
	 */
	
	public Preuve(Formule premisses, Formule conclusion){
		this.premisses = premisses;
		this.conclusion = conclusion;
	}
	
	/*
	 * Accesseurs
	 */
	
	public Formule getPremisses() {
		return premisses;
	}

	public Formule getConclusion() {
		return conclusion;
	}
	
	/*
	 * Services
	 */
	
	public void doPreuve(){
		/*	formeClausalePremisses();
			negationConclusion();
			supprConnecteurs();
			descendreNegation();
			transportQuantificateurs();
			miseFormeSkolem();
			miseFormeStandart();
			miseFormeClausale();
		*/
		System.out.println("//////////////////////////////");
		System.out.println("// ETAPE 1 - MODELISATION : //");
		System.out.println("//////////////////////////////");
		System.out.println();
		System.out.println("Premisses : "+premisses);
		System.out.println("Conclusion : "+conclusion);
		System.out.println();
		System.out.println();
		
		System.out.println("////////////////////////////////////////////////////////////////");
		System.out.println("// ETAPE 2 - FORME CLAUSALE PREMISSES + NEGATION CONCLUSION : //");
		System.out.println("////////////////////////////////////////////////////////////////");
		System.out.println();
		formeClausalePremisses();
		System.out.println();
		negationConclusion();
		System.out.println();
		System.out.println();
		
		System.out.println("/////////////////////////////////////////");
		System.out.println("// ETAPE 3 - PREUVE INSATISFIABILITE : //");
		System.out.println("/////////////////////////////////////////");
		System.out.println();
		supprConnecteurs();
		System.out.println();
		descendreNegation();
		System.out.println();
		transportQuantificateurs();
		System.out.println();
		miseFormeSkolem();
		System.out.println();
		miseFormeClausale();
		System.out.println();
		System.out.println();
	}

	public void formeClausalePremisses(){
		System.out.println("2.1)");
		System.out.println("Forme clausale des premisses en cours de développement...");
	}
	
	public void negationConclusion(){
		conclusion = conclusion.negation();
		System.out.println("2.2)");
		System.out.println("Négation de la conclusion : "+conclusion);
	}
	
	public void supprConnecteurs(){
		premisses = premisses.supprimeConnecteurs();
		conclusion = conclusion.supprimeConnecteurs();
		System.out.println("3.1)");
		System.out.println("Suppression connecteurs sur les premisses : "+premisses);
		System.out.println("Suppression connecteurs sur la conclusion : "+conclusion);
	}
	
	public void descendreNegation(){
		premisses = premisses.descendreNegation(false);
		conclusion = conclusion.descendreNegation(false);
		System.out.println("3.2)");
		System.out.println("Descendre les négations sur premisses : "+premisses);
		System.out.println("Descendre les négations sur conclusion : "+conclusion);
	}
	
	public void transportQuantificateurs(){
		//premisses = premisses.procedureTransportQ();
		//conclusion = conclusion.procedureTransportQ();
		
		// Test 
		for (int i=0;i<10;i++){
			premisses = premisses.transportQuantificateurs();
			conclusion = conclusion.transportQuantificateurs();
		}
		// Fin du test
		System.out.println("3.3)");
		System.out.println("Transport des quantificateurs sur premisses : "+premisses);
		System.out.println("Transport des quantificateurs sur conclusion : "+conclusion);
	}
	
	public void miseFormeSkolem(){
		//premisses = premisses.miseFormeSkolem();
		//conclusion = conclusion.miseFormeSkolem();
		
		System.out.println("3.4)");
		System.out.println("En cours de développement...");
		System.out.println();
		System.out.println("Mise sous forme Skolem sur premisses : "+premisses);
		System.out.println("Mise sous forme Skolem sur conclusion : "+conclusion);
	}
	
	public void miseFormeClausale(){
		//premisses = premisses.miseFormeClausale();
		//conclusion = conclusion.miseFormeClausale();
		
		System.out.println("3.5)");
		System.out.println("En cours de développement...");
		System.out.println();
		System.out.println("Mise sous forme Clausale sur premisses : "+premisses);
		System.out.println("Mise sous forme Clausale sur conclusion : "+conclusion);
	}
}